(declare-fun x () (Seq (Seq Int)))
(declare-fun xp () (Seq (Seq Int)))
(declare-fun z () (Seq Int))
(declare-fun n () Int)
(declare-fun l0 () Bool)
(declare-fun l1 () Bool)
(declare-fun l3 () Bool)
(declare-fun l4 () Bool)
(declare-fun l5 () Bool)
(assert (not (= (seq.unit 1) (seq.extract z 0 1))))
(assert (= l5 l0))
(assert (not (= (seq.extract z n 1) (seq.unit 0))))
(assert (= l4 (= x (seq.++ xp (seq.unit z)))))
(check-sat)
